$\forall$$A$, $B$:Type, $Q$:($A$$\rightarrow$$B$$\rightarrow\mathbb{P}$). ($\forall$$x$:$A$. $\exists$$y$:$B$. $Q$($x$,$y$)) $\Rightarrow$ ($\exists$$f$:$A$$\rightarrow$$B$. ($\forall$$x$:$A$. $Q$($x$,$f$($x$))))